% -*- prolog -*-
%
%

%:- use_module('rp2.pl').

:- module(rp2_type,
	[type/1,
	construct_term/3,
	construct_term_list/2,
	construct_term_list/3,
	extract_types_from_term/3,
	extract_types/2,
	reset_depth/0,
	specialtype/1,
	applytypes/1]).


:- use_module(library(lists)).
:- use_module(library(assoc)).
:- use_module(library(atts)).
:- use_module(library(terms)).
:- use_module(library(ugraphs)).

:- yap_flag(profiling,on).
:- yap_flag(unknown,error).
:- yap_flag(single_var_warnings,on).


:- multifile user:term_expansion/2.
:- multifile user:goal_expansion/3.
:- multifile rp2_type:construct_term/4.

:- op(1130,fx,[type,forward,specialtype]).

:- op(1110,xfx,['--->','===']).


:- op(150,fy,'@').
:- op(149,xfy,'@').

:- initialization(init).

init :-
	richprolog:rp_version(V), % XXX - this won't be needed soon ...
	% format('[ RichProlog2 enumerated types ~p ]~n',[V]),
	% initialise type system store
	empty_assoc(Types),  % I don't know why the assoc: here is needed ...
	bb_put(type_tree,Types),
	bb_put(contains_graph,[]),
	bb_put(subtype_graph,[]),
	numbervars(Var,0,_),
	asserta(varTID(@Var)),
	store_variable_type,
	install_term_expander. % this ensures only the user program gets terms expanded ...

dump_graphs :-
	bb_get(contains_graph,CG),
	bb_get(subtype_graph,SG),
	findall(Types,recorded(typekey,Types,_),TT),
	findall(Aliases,recorded(alias,Aliases,_),AA),
	format('Contains: ~p~n SubType: ~p~n Type Tree: ~p~n Aliases: ~p~n',[CG,SG,TT,AA]).

forward A :- 
	is_type_syntax(A),
        format_i(3,'forward declaration of type - ~p~n',[A]),
	%(functor(A,_,0) ->
	    %add_parse_ability(A);
	    %true),
	add_forward_declaration(A).

specialtype A :- 
	is_type_syntax(A),
        format_i(3,'specialtype declaration of type ~p~n',[A]),
	%add_parse_ability(A),
	add_special_type(A),
	!.

type A ---> B :- 
	is_type_syntax(A),
	format_i(3,'type defined; ~p is a disjunction of ~p~n',[A,B]),
	%add_parse_ability(A),
	add_type_definition(A,B),
	!.

type A ---> B :-
	rp_syntax_error('Illegal Type Definition',(type A ---> B)).

type A === B :- 
	is_lhs_alias_type_syntax(A), % @nt(@Var1,@Var2, ... , @VarN)
	identical_variables(A,B),
	add_type_alias(A,B),
	format_i(3,'alias defined; ~p is an alias of ~p~n',[A,B]),
	!.

type A === B :-
	rp_syntax_error('Illegal Type Definition',(type A === B)).

type A :-
	rp_syntax_error('Illegal Type Definition',(type A)).

% This next bit is now a syntactic convienience - restore it if it looks good
%  in the new type system
%
%add_parse_ability(@ F) :-
%	\+ current_op(_,_,F),
%	op(25,fx,F).
%
%add_parse_ability(@ F) :-
%	current_op(_,_,F).
%
%
% the first checks that the syntax of the type is correct; the second that
% this is a correctly compiled type.
%

is_type_syntax(@ _).

is_type(_). % XXX - stub for now

is_lhs_alias_type_syntax(A) :-
	term_variables(A,VarList),
	@B = A,
	B =.. [ _ | VarTypes ],
	lhs_vars_correct(VarTypes,VarList).

lhs_vars_correct([],[]).

lhs_vars_correct( [ @ T | TRest ], VarList ) :-
	vselect(T,VarList,NVL),
	lhs_vars_correct(TRest,NVL).

%
% Constructs a canonical type name
%
typestring(TypeList,TSL,VarList) :-
	term_variables(TypeList,VarList),
	copy_term(TypeList,NTL),
	numbervars(NTL,0,_),
	ts1(NTL,TSL).

ts1([],[]).
ts1([T|R],[NT|NR]) :-
	typestring1(T,NT),
	ts1(R,NR).

typestring1(A,A). % this is meant to turn a functor into something easily indexible.  Blank for now.
%typestring1(@Type, TS) :-
%	% \+ var(Type), - var is impossible since we've numbervars above
%	Type =.. [H|R],
%	length(R,Args),
%	ts1(R,NR),
%	append([H/Args],[NR],TS).

ground_type(type(T,F,_)) :-
	T \== special,
	ground(F).

atomic_type(@TID) :- atomic(TID).

type_functor(@TID,F) :- functor(TID,F,_).

%
% unify_type; check_type; apply_type need to be done
%

% build_type depends on global changes in store_type_definition
% - note '@' is stripped before we call build_type
% currently effectively both parts of a type must be ground.  It would be good 
% to remove this restriction at some stage.

add_type_alias(TypeString1,TypeString2) :-
	%typestring([TypeString2],[TID2],_),
	typestring([TypeString1],[TID1],_),
	add_subtype(TypeString2,TypeStringl,TIDl), % effectively construct new type in here ...
	store_alias(TID1,TypeString1,TIDl,TypeStringl).

add_special_type(ST) :-
	typestring([ST],[STID],VarList),
	store_type_definition(ST,STID,VarList,special),
	varTID(VTID),
	store_subtype(VTID,STID),
	store_subtype(STID,STID).

add_subtype(TypeString,TypeStringl,TIDl) :-
	typestring([TypeString],[_],VarList),
	lookup_type_with_unification(TypeString,Type),
	Type = type(TIDSuper,TypeStringl,_,CD),
	typestring([TypeStringl],[TIDl],VarList),
	store_type_definition_if_neeeded(TypeStringl,TIDl,VarList,CD),
	store_subtype(TIDSuper,TIDl),
	store_subtype(TIDl,TIDl),
	varTID(VTID),
	store_subtype(VTID,TIDl).

add_type_definition(TypeString,Definition) :-
	add_forward_declaration(TypeString),
	typestring([TypeString],[TID],VarList),
	compile_definition(Definition,CD,_),
	store_subtype(TID,TID),
	varTID(VTID),
	store_subtype(VTID,TID),
	store_type_definition(TypeString,TID,VarList,CD).

store_type_definition_if_neeeded(TypeString2,TID2,VarList2,CD) :-
	\+ lookup_type(TID2,_),
	store_type_definition(TypeString2,TID2,VarList2,CD).

store_type_definition_if_neeeded(TypeString2,TID2,_,CD) :-
	lookup_type(TID2,type(TIDl,TypeStringl,_,CDl)),
	TIDl == TID2,
	copy_variant_term(TypeStringl,TypeString2),
	copy_variant_term(CD,CDl).

copy_variant_term(T1,T2) :-
	copy_term(T1,TT),
	variant(TT,T2).

add_forward_declaration(TypeString) :-
	typestring([TypeString],[TID],VarList),
	store_forward_declaration(TypeString,TID,VarList).

add_special_type(A) :- % XXX - incomplete
	Type = type(special,A),
	store_type_definition(Type).

replace(Comp,Atom,Comp,Atom).
replace(Comp,_,Comp2,Comp2) :- Comp \= Comp2.


%
% Note - this will eventually be moved to recorda/recorded - the tree makes debugging a 
%  bit easier for now. XXX - this only now applies to subtypes ...
%
% all database *keys* have no preceeding @ - these are added + deleted by
% store-type-defintion - this will make indexing quicker in the final implementation
%
% Also note the order of TID is set so ground things occur earlier in the list;
%  this should ticke the sweet spot in the recorda/recorded implementation.
%

% using recordz is important here - since supertypes must be defined before
% subtypes, this assures that we get the MGU in the list of possible unifiers
% when we call lookup_type_with_unification

store_variable_type :-
	varTID(TID),
	(\+ recorded(typekey,type(TID,_,_,_),_) ->
	 recorda(typekey,type(TID,@X,[X],[@var]),_); true).

remove_variable_type :-
	varTID(TID),
	(recorded(typekey,type(TID,_,_,_),Ref) -> erase(Ref) ; true).

store_type_definition(TypeString,TID,VarList,CD) :-
	(\+ recorded(typekey,type(TID,TypeString,_,_),_);
	    recorded(typekey,type(TID,TypeString,_,forward),Ref),
	    erase(Ref)),
	%remove_variable_type,
	recorda(typekey,type(TID,TypeString,VarList,CD),_).
	%store_variable_type.

store_forward_declaration(TypeString,TID,VarList) :-
	(\+ recorded(typekey,type(TID,TypeString,_,_),_);
	    recorded(typekey,type(TID,TypeString,_,forward),Ref),
	    erase(Ref)),
	recorda(typekey,type(TID,TypeString,VarList,forward),_).

store_alias(TID1,TypeString1,TID2,TypeString2) :-
	lookup_type(TID2,_), % type 2 must be a valid type
	recordz(alias,alias(TID1,TID2,TypeString1,TypeString2),_).

store_type_containment(TID,TypeList) :-
	bb_get(contains_graph,G0),
	bb_put(contains_graph,[TID-TypeList|G0]).

store_subtype(SuperTID, SubTID) :-
	bb_get(subtype_graph,SG),
	add_edges(SG,[SuperTID-SubTID],NSG),
	transitive_closure(NSG,TNSG),
	bb_put(subtype_graph,TNSG).

is_subtype(SuperTID, SubTID) :-
	bb_get(subtype_graph,SG),
	edges(SG,E),
	memberchk(SuperTID-SubTID,E).

get_disjunct(TID,C) :- % this doesn't check currently that a type is ground
	lookup_tid(TID,type(_,_,_,CD)),
	member(C,CD).

lookup_tid(TID1,Desc) :-
	Desc1 = alias(TID1,TID2,_,_),
	recorded(alias,Desc1,_),
	lookup_tid(TID2,Desc),!.

lookup_tid(TID,Desc) :-
	Desc = type(TID,_,_,_),
	recorded(typekey,Desc,_),!.

lookup_type(Type,Desc) :-
	typestring([Type],[TID],_),
	lookup_tid(TID,Desc).

lookup_type_with_unification(TypeString,Desc) :-
	Desc1 = alias(_,_,TypeString,TypeString2),
	recorded(alias,Desc1,_),
	lookup_type_with_unification(TypeString2,Desc).

lookup_type_with_unification(TypeString,Desc) :-
	Desc = type(_,TypeString,_,_),
	recorded(typekey,Desc,_).


% this should work as:
% type t(X) ---> 0; @t1; s(s(@t2)); q(@X).
%  [ 0, @t1, s(s(@t2)), q(@X) ]
%

compile_definition(D,CD,TypeList) :-
	richprolog:disj_list(D,CL),
	cd1(CL,CD,TypeList0),
	sort(TypeList0,TypeList).

cd1([],[],[]).

cd1([H|R],[NH|NR],TypeList) :-
	rd1(H,NH,TypeList0),
	cd1(R,NR,TypeList1),
	append(TypeList0,TypeList1,TypeList).

rd1(@var, disjunct(@var,[]),[]) :- !.

rd1( X, disjunct(TID,[]),[TID]) :- 
	is_type_syntax(X), 
	lookup_type(X,type(TID,_,_,_)),
	!.

rd1( X , disjunct(H,R),TypeList) :- 
	X =.. [H|R0],
	ad1(R0,R,TypeList).

ad1([],[],[]).

ad1([@V|R],[@V|NR],[@V|T]) :-
	var(V),
	ad1(R,NR,T).

ad1([H|R],[NH|NR],[NH|T]) :-
	is_type_syntax(H), 
	!,
	lookup_type_with_unification(H,type(_,NH,_,_)),
	ad1(R,NR,T).

ad1([H|R],[H|NR],T) :-
	\+ is_type_syntax(H),
	ad1(R,NR,T).

/*
*  Type-checking unifier - not yet complete - needs to comprehend 
*  sub-types
*/

:- attribute richprolog_type/1.

verify_attributes(Var,Val,Goals) :-
	%print('Verifying ...\n'),
	get_atts(Var,richprolog_type(Type)),
	!,
	( var(Val) ->
	    !,
	    (  get_atts(Val,richprolog_type(OtherType)) ->
		   (is_subtype(Type,OtherType) ->
		       Goals = [put_atts(Var,[richprolog_type(OtherType)])]
		       ;
                    (is_subtype(OtherType,Type) ->
		       Goals = [put_atts(Var,[richprolog_type(Type)])]
		       ;
		       fail )
		    )
		;
		   (Goals = [put_atts(Val,[richprolog_type(Type)])])

	    )
	 ;
	 (  typeok(Type,Val),
	   %print('Verifying 2 ...\n'),
	   Goals = [],!)
       ).

verify_attributes(_,_,[]) :-
	print('Verification retry - should not happen ...\n').	

attribute_goal(Var,Var@TID) :-
	get_atts(Var,richprolog_type(@TID)).

%
% note that only variables have types bound to them
%  - they include the @ as well
%
typeof(TID,Variable) :-
	var(Variable),
	\+ get_atts(Variable,[richprolog_type(TID)]),
	put_atts(Variable,[richprolog_type(TID)]).

typeof(TID,Variable) :-
	var(Variable),
	get_atts(Variable,[richprolog_type(TID)]).

check_type(TID,Variable) :-
	var(Variable),
	get_atts(Variable,[richprolog_type(TID)]).

%
% currently only typedefs are known to be decidible
%
known_decidible(V @ T) :- 
	is_type_syntax(@T),
	var(V).

% compiler to be built ...
install_type_checker(type(_,_,_)).

applytypes([]).
applytypes([H|R]) :-
	call(H),
	applytypes(R).

% should this be "type(T)" or "T@type?" - both for now ...
%
user:goal_expansion(T @ TypeString, M, M:Goal) :-
	rp2_type:typestring([@TypeString],[TID],_),
	(rp2_type:lookup_tid(TID,type(TIDl,_,_,_)) ->
	    (TIDFinal = TIDl);
	    (rp2_type:add_subtype(@TypeString,_,TIDl),TIDFinal = TIDl)
	    ),
	Goal = (rp2_type:typeok(TIDFinal,T)).

/*
* In future pre-compile these with a goal-expansion; will save calls to member/2
*/

:- multifile typeok/2.


typeok(TID,Term) :- 
	var(Term),
	!,
	typeof(TID,Term).

typeok(TID,Term@Type) :-
	!,
	lookup_tid(TID,type(_,@Type,_,_)),
	typeok(TID,Term).

typeok(TID,Term) :-
	\+ var(Term),
	varTID(TID).

typeok(TID,Term) :-
	\+ var(Term),
	\+ is_type_syntax(Term), % - XXX - change so it's looking for a ground part of a term
	Term =.. [Head|Args],
	get_disjunct(TID,disjunct(Head,TIDList)), % note get_disjunct has no @
	argsok(TIDList,Args).

typeok(TID,Term) :-
	\+ var(Term),
	\+ is_type_syntax(Term),
	Term =.. [_|Args],
	get_disjunct(TID,disjunct(NewTID,TIDList)), % note get_disjunct has no @
	is_type_syntax(NewTID),
	typeok(NewTID,Term),
	argsok(TIDList,Args).

typeok(TermA, TermB) :-
	\+ var(TermB),
	\+ is_type_syntax(TermA), % - XXX - change so it's looking for a ground part of a term
	TermA =.. [Head|ArgsA],
	TermB =.. [Head|ArgsB],
	argsok(ArgsA,ArgsB).

argsok([],[]) :- !.

argsok([H|R],[TH|TR]) :-
	typeok(H,TH),
	!,
	argsok(R,TR).

current_depth(N) :-
	recorded(rp_depth,N,K),
	erase(K),
	NN is N + 1,
	recorda(rp_depth,NN).
current_depth(0) :-
	\+ recorded(rp_depth,_,_),
	recorda(rp_depth,1).

reset_depth :-
	recorded(rp_depth,_,K),
	erase(K),!.

reset_depth.

construct_term_list(T,V) :-
	repeat,
	current_depth(D),
	construct_term_list(T,V,D,0).

construct_term_list(T,V,Depth) :-
	construct_term_list(T,V,Depth,_).

construct_term_list([],[],N,N).
construct_term_list([T|TR],[V|VR],D0,D) :-
	construct_term(T,D0,D1,V),
	construct_term_list(TR,VR,D1,D).

construct_term(Type,Term,Max) :- construct_term(Type,Max,_,Term).

:- multifile construct_term/4.

construct_term(@var,A,A,@var) :- !.

construct_term(TID,OldArity,NewArity,Term) :-
	is_type_syntax(TID),
	get_disjunct(TID,disjunct(Head,TypeList)),
	NA0 is OldArity - 1,
	NA0 >= 0,
	(is_type_syntax(Head) ->
	    (Head == @var ->
		(Term = _ , NewArity = NA0);
		construct_term(Head,NA0,NewArity,Term)
	     )
	 ;
	     (construct_arguments(TypeList,NA0,NewArity,Args),
	     Term =.. [Head|Args])
         ).

construct_term(Ground,A,A,Ground) :-
	\+ is_type_syntax(Ground).

construct_arguments([],NA,NA,[]).

construct_arguments([H|R],NA0,NA,[NH|NR]) :-
	construct_term(H,NA0,NA1,NH),
	construct_arguments(R,NA1,NA,NR).

% XXX - see how this interacts with the syntax checker

install_term_expander :-
	asserta((
	 user:term_expansion((H :- B), (NH :- NB) ) :-
	        !,
	        type_term_expansion((H :- B), (NH0 :- NB0)),
		richprolog:syntax_term_expansion((NH0 :- NB0),(NH :- NB))
        )),
	asserta((
          user:term_expansion(X,(NH :- NB)) :-
	        \+ functor(X,':-',2),
		type_term_expansion(X,(NH0 :- NB0)),
		!,
		richprolog:syntax_term_expansion((NH0 :- NB0),(NH :- NB))
	)),
	asserta((
          user:term_expansion(X,X1) :-
	        \+ functor(X,':-',2),
		% \+ type_term_expansion(X,(NH0 :- NB0)),
		!,
		richprolog:syntax_term_expansion_fact(X,X1)
	)).


type_term_expansion((H :- B), (NH :- NB)) :-
	richprolog:clause_list(B, GL),
	extract_types_from_term(H,NH,HT),
	extract_types(GL,NGL0),
	append(HT,NGL0,NGL),
	richprolog:clause_list(NB, NGL).


type_term_expansion(X,(NH :- HT)) :-
	\+ functor(X,':-',_),
	extract_types_from_term(X,NH,HTL),
	richprolog:clause_list(HT, HTL).

extract_types([GF|GR],NG) :-
	extract_types_from_term(GF,NGF0,Types),
	append(Types,[NGF0],NGF),
	extract_types(GR,NGR),
	append(NGF,NGR,NG).
	%format('New goal is ~p~n',[NG]).

extract_types([],[]).

extract_types_from_term(X,NX,Types) :-
	X =.. [H|R],
	extract_types(R,NR,Types),
	NX =.. [H|NR].

extract_types([Term|TermRest],[NT|NTRest],Types) :-
	extract_type(Term,NT,NType),
	extract_types(TermRest,NTRest,NTypes),
	append(NType,NTypes,Types).

extract_types([],[],[]).

% is it a typed variable
extract_type(Var,Var,[]) :-
	(var(Var),!);(richprolog:term_frozen_var(Var),!).

extract_type(Var@Type,Var,[Var@Type]) :-
	(var(Var),!);(richprolog:term_frozen_var(Var),!).

extract_type(Term@Type,NewTerm,[NewTerm@Type|Types]) :-
	!,
	extract_type(Term,NewTerm,Types).
	

extract_type(Term,NewTerm,Type) :-
	compound(Term),
	!,
	extract_types_from_term(Term,NewTerm,Type).

extract_type(Term,Term,[]).

% identical_variables - check that two terms have the same variables

identical_variables(T1,T2) :-
	term_variables(T1,V1),
	term_variables(T2,V2),
	ident_vars(V1,V2).

ident_vars([],[]).

ident_vars([HV|RV],OV) :-
	vselect(HV,OV,NOV),
	ident_vars(RV,NOV).

vselect(Var,OldL,NewL) :-
	vselect(Var,[],OldL,NewL).


vselect(Var,NotVar,[OldH|OldR],NewL) :-
	Var == OldH,
	append(NotVar,OldR,NewL).

vselect(Var,NotVar,[OldH|OldR],NewL) :-
	Var \== OldH,
	vselect(Var,[OldH|NotVar],OldR,NewL).


%
% constraint printer for yap/clp(q,r)
%

dump_constraints(ExistVars) :-
	copy_term_workaround(ExistVars,NEV),
	flatten(NEV,FlatEV),
	non_vars(FlatEV,NonVars),
	%length(FlatEV,1),
	dump(NonVars,NonVars,Printer),
	write(Printer).

dump(_,_,_).

% format_i(X,Y,Z) :- richprolog:format_i(X,Y,Z).




